{- Write a function for checking whether two Boolean formulas are equivalent.
  Use Haskell.  
  Deliverables: program with documentation, indication of time spent. -}

module Assignment1 where

import Parser
import List

logicalEquivalence :: Form -> Form -> Bool
logicalEquivalence f1 f2 = solve (Equiv f1 f2)
-- For each Prop X assign the values true and false. Make sure to generate
-- every possible combinations of true false pairs for all variables.

solve :: Form -> Bool
solve (Value v) = v
solve (Cnj f) = and(map solve f)
solve (Dsj f) = or(map solve f)
solve (Impl f1 f2) = (not (solve f1)) || solve f2
solve (Equiv f1 f2) = solve f1 == solve f2

getLiterals :: Form -> [Form]
getLiterals (Prop x) = [(Prop x)]
getLiterals (Cnj fs) = nub (concat (map getLiterals fs))
getLiterals (Dsj fs) = nub (concat (map getLiterals fs))
getLiterals (Impl f1 f2) = nub (getLiterals f1 ++ getLiterals f2)
getLiterals (Equiv f1 f2) = nub (getLiterals f1 ++ getLiterals f2)

-- Takes a list of proposition letters as input, and produces a truth table
-- consisting of a list of lists.
truthTable :: [Form] -> [[(Form,Bool)]]
truthTable ps = split (length ps) (possibilities ps [])
                
possibilities :: [Form] -> [(Form,Bool)] -> [(Form,Bool)]
possibilities [] prefix = prefix
possibilities ps prefix = possibilities (tail ps) (prefix ++ [(head ps,True)]) ++ 
                          possibilities (tail ps) (prefix ++ [(head ps,False)])

-- This function was taken from the module Data.List.Split. This module is not
-- installed by default, so we copied it here to not have the dependency.
split :: Int -> [a] -> [[a]]
split n = unfoldr (\r -> case r of [] -> Nothing; x -> Just $ splitAt n x)

{-
We have finished checking the equivalence of a formula with predefined boolean
values. We are able of generating truth tables. However, we were unable to
finish the code used for filling in formulas with the generated truth tables.

Indication of time spent for all three assignments: 16 hours per person.
-}
